lpath($p$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\forall$$i$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$p$$\parallel-$1}}$. destination($p$[$i$]) $=$ source($p$[$i$+1]) \& $\neg$$p$[$i$+1] $=$ lnk{-}inv($p$[$i$])